(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
p(0) → 0
p(s(X)) → X
leq(0, Y) → true
leq(s(X), 0) → false
leq(s(X), s(Y)) → leq(X, Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
diff(X, Y) → if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y)))
0 → n__0
s(X) → n__s(X)
diff(X1, X2) → n__diff(X1, X2)
p(X) → n__p(X)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__diff(X1, X2)) → diff(activate(X1), activate(X2))
activate(n__p(X)) → p(activate(X))
activate(X) → X
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
activate(n__s(n__diff(X126897_3, X226898_3))) →+ s(if(leq(activate(X126897_3), activate(X226898_3)), n__0, n__s(n__diff(n__p(activate(X126897_3)), activate(X226898_3)))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [X126897_3 / n__s(n__diff(X126897_3, X226898_3))].
The result substitution is [ ].
The rewrite sequence
activate(n__s(n__diff(X126897_3, X226898_3))) →+ s(if(leq(activate(X126897_3), activate(X226898_3)), n__0, n__s(n__diff(n__p(activate(X126897_3)), activate(X226898_3)))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,2,0,0,0].
The pumping substitution is [X126897_3 / n__s(n__diff(X126897_3, X226898_3))].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)